package com.ecnu.codelearn.software_analysis;

import org.apache.commons.lang3.StringUtils;

import java.io.Serializable;
import java.util.ArrayList;
import java.util.HashMap;
import java.util.HashSet;
import java.util.LinkedHashMap;
import java.util.LinkedHashSet;
import java.util.List;
import java.util.Map;
import java.util.Set;

/**
 * KS结构中R部分的数据结构，也就是所有的变迁关系（为图形结构）
 */
public class KripkeStructure implements Serializable {
    private static final String INACTIVATED = "inactivated";

    /**
     * 顶点，
     * 串行程序时为pc值
     * 并发程序由共享变量+,+第一个程序的pc值+,+第二个程序的pc值组成
     */
    private String vertex;
    /**
     * 共享变量
     */
    private String turn;
    /**
     * 子程序的pc标记值（只在并发时有数据，且由题意，这里有且只有两个数据，第一个是p0的pc值，第二个是p1的pc值）
     */
    private List<String> subMarkList;
    /**
     * 当前顶点的下一跳的顶点集合
     */
    private List<KripkeStructure> nextKripkeStructureList;

    public KripkeStructure(String vertex) {
        this.vertex = vertex;
    }

    public KripkeStructure(String vertex, String turn, String p0Mark, String p1Mark) {
        this.vertex = vertex;
        this.turn = turn;
        subMarkList = new ArrayList<>();
        this.subMarkList.add(p0Mark);
        this.subMarkList.add(p1Mark);
    }

    /**
     * 从并发的一阶逻辑公式中获取KS的R数据
     * @param resultFirstOrder
     * @return
     */
    public static List<KripkeStructure> getConcurrentKSFromFirstOrderLogic(List<FirstOrderLogic> resultFirstOrder) {
        List<KripkeStructure> kripkeStructureList = new ArrayList<>();//用于返回的集合数据


        String turn0 = "";//p0的共享变量的赋值（一阶逻辑中wait里边的内容）
        String turn1 = "";//p1的共享变量的赋值（一阶逻辑中wait里边的内容）

        Map<String, FirstOrderLogic> p0InMarkMap = new LinkedHashMap<>();
        Map<String, FirstOrderLogic> p1InMarkMap = new LinkedHashMap<>();

        Map<String, List<FirstOrderLogic>> firstOrderInMarkMap = new LinkedHashMap<>();//key为所有一阶逻辑的入状态（pc0，pc1的所有状态），value为这个入状态，对应的

        for (int i = 2; i < resultFirstOrder.size(); i++) {//前边两个一阶逻辑公式是程序的入口和出口，这里不做考虑，下标从2开始
            FirstOrderLogic firstOrderLogic = resultFirstOrder.get(i);

            List<String> subInMarkList = firstOrderLogic.getSubInMarkList();

            for (int j = 0; j < subInMarkList.size(); j++) {
                String subInMark = subInMarkList.get(j);
                if (StringUtils.isBlank(subInMark)) {
                    continue;
                }
                if (j == 0) {
                    if (p0InMarkMap.containsKey(subInMark)) {
                        p0InMarkMap.put(subInMark, firstOrderLogic);
                    } else {
                        p0InMarkMap.put(subInMark, firstOrderLogic);
                    }
                    if (StringUtils.isNoneBlank(firstOrderLogic.getTurn())) {
                        turn0 = firstOrderLogic.getTurn();
                    }
                } else {
                    if (p1InMarkMap.containsKey(subInMark)) {
                        p1InMarkMap.put(subInMark, firstOrderLogic);
                    } else {
                        p1InMarkMap.put(subInMark, firstOrderLogic);
                    }
                    if (StringUtils.isNoneBlank(firstOrderLogic.getTurn())) {
                        turn1 = firstOrderLogic.getTurn();
                    }
                }

            }

            for (String subInMark : subInMarkList) {
                if (StringUtils.isBlank(subInMark)) {
                    continue;
                }
                if (firstOrderInMarkMap.containsKey(subInMark)) {
                    firstOrderInMarkMap.get(subInMark).add(firstOrderLogic);
                } else {
                    List<FirstOrderLogic> list = new ArrayList<>();
                    list.add(firstOrderLogic);
                    firstOrderInMarkMap.put(subInMark, list);
                }
            }
        }


        Map<String, KripkeStructure> ksStatusMap = new HashMap<>();//顶点的备份，这个map的值中存的下一跳为空，为了防止出现回路，否则后台无法将数据打印为json返给前端
        //设置顶点（p0）
        for (Map.Entry<String, FirstOrderLogic> p0Entry : p0InMarkMap.entrySet()) {
            for (Map.Entry<String, FirstOrderLogic> p1Entry : p1InMarkMap.entrySet()) {
                //设置顶点
                String vertex = turn0 + "," + p0Entry.getKey() + "," + p1Entry.getKey();
                KripkeStructure kripkeStructure = new KripkeStructure(vertex, turn0, p0Entry.getKey(), p1Entry.getKey());
                kripkeStructureList.add(kripkeStructure);

                //设置顶点的备份
                kripkeStructure = new KripkeStructure(vertex, turn0, p0Entry.getKey(), p1Entry.getKey());//这里新new一个，是为了防止出现回路，否则后台无法将数据打印为json返给前端
                ksStatusMap.put(vertex, kripkeStructure);

                if (StringUtils.isNotBlank(p1Entry.getValue().getTurn())) {
                    break;//共享变量为p0的turn时，pc1状态不能跑到p1程序wait语句的后面
                }
            }
        }
        //设置顶点（p1）
        for (Map.Entry<String, FirstOrderLogic> p1Entry : p1InMarkMap.entrySet()) {
            for (Map.Entry<String, FirstOrderLogic> p0Entry : p0InMarkMap.entrySet()) {
                String vertex = turn1 + "," + p0Entry.getKey() + "," + p1Entry.getKey();
                KripkeStructure kripkeStructure = new KripkeStructure(vertex, turn1, p0Entry.getKey(), p1Entry.getKey());
                kripkeStructureList.add(kripkeStructure);
                kripkeStructure = new KripkeStructure(vertex, turn1, p0Entry.getKey(), p1Entry.getKey());
                ksStatusMap.put(vertex, kripkeStructure);

                if (StringUtils.isNotBlank(p0Entry.getValue().getTurn())) {
                    break;//共享变量为p1的turn时，pc0状态不能跑到p0程序wait语句的后面
                }
            }
        }

        //设置边
        for (KripkeStructure kripkeStructure : kripkeStructureList) {//循环顶点，设置顶点的下一跳的集合
            String turn = kripkeStructure.turn;
            List<String> subMarkList = kripkeStructure.subMarkList;
            String p0Mark = subMarkList.get(0);
            String p1Mark = subMarkList.get(1);

            List<KripkeStructure> nextKripkeStructureList = new ArrayList<>();

            //设置当前顶点pc0的下一跳
            List<FirstOrderLogic> p0FirstOrderLoginList = firstOrderInMarkMap.get(p0Mark);
            for (FirstOrderLogic firstOrderLogic : p0FirstOrderLoginList) {
                List<String> subOutMarkList = firstOrderLogic.getSubOutMarkList();
                for (String nextP0Mark : subOutMarkList) {
                    if (StringUtils.isBlank(nextP0Mark)) {
                        continue;
                    }

                    if (StringUtils.isNotBlank(turn) && StringUtils.isNotBlank(firstOrderLogic.getTurn())) {
                        if (!turn.equals(firstOrderLogic.getTurn()) && !firstOrderLogic.getSubInMarkList().get(0).equals(firstOrderLogic.getSubOutMarkList().get(0))) {
                            continue;
                        }
                        if (turn.equals(firstOrderLogic.getTurn()) && firstOrderLogic.getSubInMarkList().get(0).equals(firstOrderLogic.getSubOutMarkList().get(0))) {
                            continue;
                        }
                    }


                    //共享变量变迁
                    String vertex = turn + "," + nextP0Mark + "," + p1Mark;
                    if (turn.equals(turn0)) {
                        if (StringUtils.isNoneBlank(firstOrderLogic.getVariablesChanged()) && turn1.contains(firstOrderLogic.getVariablesChanged())) {
                            vertex = turn1 + "," + nextP0Mark + "," + p1Mark;
                        }
                    } else {
                        if (StringUtils.isNoneBlank(firstOrderLogic.getVariablesChanged()) && turn0.contains(firstOrderLogic.getVariablesChanged())) {
                            vertex = turn0 + "," + nextP0Mark + "," + p1Mark;
                        }
                    }

                    KripkeStructure nextKripkeStructure = ksStatusMap.get(vertex);
                    if (nextKripkeStructure == null) {
                        continue;
                    }
                    nextKripkeStructureList.add(nextKripkeStructure);
                }
            }

            //设置当前顶点pc1的下一跳
            List<FirstOrderLogic> p1FirstOrderLoginList = firstOrderInMarkMap.get(p1Mark);
            for (FirstOrderLogic firstOrderLogic : p1FirstOrderLoginList) {
                List<String> subOutMarkList = firstOrderLogic.getSubOutMarkList();
                for (String nextP1Mark : subOutMarkList) {
                    if (StringUtils.isBlank(nextP1Mark)) {
                        continue;
                    }

                    if (StringUtils.isNotBlank(turn) && StringUtils.isNotBlank(firstOrderLogic.getTurn())) {
                        if (!turn.equals(firstOrderLogic.getTurn()) && !firstOrderLogic.getSubInMarkList().get(1).equals(firstOrderLogic.getSubOutMarkList().get(1))) {
                            continue;
                        }
                        if (turn.equals(firstOrderLogic.getTurn()) && firstOrderLogic.getSubInMarkList().get(1).equals(firstOrderLogic.getSubOutMarkList().get(1))) {
                            continue;
                        }
                    }

                    //共享变量变迁
                    String vertex = turn + "," + p0Mark + "," + nextP1Mark;
                    if (turn.equals(turn0)) {
                        if (StringUtils.isNoneBlank(firstOrderLogic.getVariablesChanged()) && turn1.contains(firstOrderLogic.getVariablesChanged())) {
                            vertex = turn1 + "," + p0Mark + "," + nextP1Mark;
                        }
                    } else {
                        if (StringUtils.isNoneBlank(firstOrderLogic.getVariablesChanged()) && turn0.contains(firstOrderLogic.getVariablesChanged())) {
                            vertex = turn0 + "," + p0Mark + "," + nextP1Mark;
                        }
                    }

                    KripkeStructure nextKripkeStructure = ksStatusMap.get(vertex);
                    if (nextKripkeStructure == null) {
                        continue;
                    }
                    nextKripkeStructureList.add(nextKripkeStructure);
                }
            }
            kripkeStructure.nextKripkeStructureList = nextKripkeStructureList;
        }

        //设置ks的入口顶点
        KripkeStructure turn0Start = new KripkeStructure(turn0 + "," + INACTIVATED + "," + INACTIVATED, turn0, INACTIVATED, INACTIVATED);
        KripkeStructure turn1Start = new KripkeStructure(turn1 + "," + INACTIVATED + "," + INACTIVATED, turn0, INACTIVATED, INACTIVATED);

        //设置ks的入口顶点的边
        List<String> subOutMarkList = resultFirstOrder.get(0).getSubOutMarkList();
        KripkeStructure turn0NextKripkeStructure = ksStatusMap.get(turn0 + "," + subOutMarkList.get(0) + "," + subOutMarkList.get(1));
        List<KripkeStructure> turn0StartNextList = new ArrayList<>();
        turn0StartNextList.add(turn0NextKripkeStructure);
        turn0Start.nextKripkeStructureList = turn0StartNextList;

        KripkeStructure turn1NextKripkeStructure = ksStatusMap.get(turn1 + "," + subOutMarkList.get(0) + "," + subOutMarkList.get(1));
        List<KripkeStructure> turn1StartNextList = new ArrayList<>();
        turn1StartNextList.add(turn1NextKripkeStructure);
        turn1Start.nextKripkeStructureList = turn1StartNextList;

        kripkeStructureList.add(turn0Start);
        kripkeStructureList.add(turn1Start);

        return kripkeStructureList;
    }

    /**
     * 从串行的一阶逻辑公式中获取KS的R数据
     * @param resultFirstOrder
     * @return
     */
    public static List<KripkeStructure> getSerialKSFromFirstOrderLogic(List<FirstOrderLogic> resultFirstOrder) {
        List<KripkeStructure> resultList = new ArrayList<>();

        Map<String, List<FirstOrderLogic>> inMarkFirstOrderLogicMap = new LinkedHashMap<>();//一个入口状态，可能对应多条一阶逻辑公式，也就是可能有多个下一跳（比如if分支的情况）
        Set<String> inMarkSet = new LinkedHashSet<>();//所有的状态集合
        for (FirstOrderLogic firstOrderLogic : resultFirstOrder) {
            String inMark = firstOrderLogic.getInMark();
            if (inMarkFirstOrderLogicMap.containsKey(inMark)) {
                inMarkFirstOrderLogicMap.get(inMark).add(firstOrderLogic);
            } else {
                List<FirstOrderLogic> list = new ArrayList<>();
                list.add(firstOrderLogic);
                inMarkFirstOrderLogicMap.put(inMark, list);
                inMarkSet.add(inMark);
            }

        }
        inMarkSet.add("e_m");//添加出口状态

        //设置顶点
        for (String inMark : inMarkSet) {
            KripkeStructure kripkeStructure = new KripkeStructure(inMark);
            resultList.add(kripkeStructure);
        }

        //设置边
        for (KripkeStructure kripkeStructure : resultList) {
            if (!inMarkFirstOrderLogicMap.containsKey(kripkeStructure.vertex)) {
                continue;
            }
            List<KripkeStructure> nextKripkeStructureList = new ArrayList<>();
            for (FirstOrderLogic firstOrderLogic : inMarkFirstOrderLogicMap.get(kripkeStructure.vertex)) {
                if (inMarkSet.contains(firstOrderLogic.getOutMark())) {
                    nextKripkeStructureList.add(new KripkeStructure(firstOrderLogic.getOutMark()));
                }
            }
            kripkeStructure.nextKripkeStructureList = nextKripkeStructureList;
        }

        return resultList;
    }

    public String getVertex() {
        return vertex;
    }

    public void setVertex(String vertex) {
        this.vertex = vertex;
    }

    public List<KripkeStructure> getNextKSStatusList() {
        return nextKripkeStructureList;
    }

    public void setNextKSStatusList(List<KripkeStructure> nextKripkeStructureList) {
        this.nextKripkeStructureList = nextKripkeStructureList;
    }

    @Override
    public String toString() {
        return "KSStatus{" +
                "vertex='" + vertex + '\'' +
//                ", turn='" + turn + '\'' +
                ", subMarkList=" + subMarkList +
                ", nextKSStatusList=" + nextKripkeStructureList +
                '}';
    }
}
